Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		le(0,y)	→ true
2:		le(s(x),0)	→ false
3:		le(s(x),s(y))	→ le(x,y)
4:		minus(0,y)	→ 0
5:		minus(s(x),y)	→ if_minus(le(s(x),y),s(x),y)
6:		if_minus(true,s(x),y)	→ 0
7:		if_minus(false,s(x),y)	→ s(minus(x,y))
8:		mod(0,y)	→ 0
9:		mod(s(x),0)	→ 0
10:		mod(s(x),s(y))	→ if_mod(le(y,x),s(x),s(y))
11:		if_mod(true,s(x),s(y))	→ mod(minus(x,y),s(y))
12:		if_mod(false,s(x),s(y))	→ s(x)

There are 8 dependency pairs:


13:		LE(s(x),s(y))	→ LE(x,y)
14:		MINUS(s(x),y)	→ IF_MINUS(le(s(x),y),s(x),y)
15:		MINUS(s(x),y)	→ LE(s(x),y)
16:		IF_MINUS(false,s(x),y)	→ MINUS(x,y)
17:		MOD(s(x),s(y))	→ IF_MOD(le(y,x),s(x),s(y))
18:		MOD(s(x),s(y))	→ LE(y,x)
19:		IF_MOD(true,s(x),s(y))	→ MOD(minus(x,y),s(y))
20:		IF_MOD(true,s(x),s(y))	→ MINUS(x,y)

The approximated dependency graph contains 3 SCCs: {13}, {14,16} and {17,19}.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {14,16}. The usable rules are {1-3}. By taking the AF π with π(le) = π(MINUS) = 1 and π(IF_MINUS) = 2 together with the lexicographic path order with precedence 0 ≻ true and s ≻ false, rule 14 is weakly decreasing and the rules in {1-3,16} are strictly decreasing.

Consider the SCC {17,19}. The usable rules are {1-7}. By taking the AF π with π(le) = π(minus) = π(MOD) = 1 and π(if_minus) = π(IF_MOD) = 2 together with the lexicographic path order with precedence s ≻ 0 ≻ true and s ≻ false, the rules in {4,5,7,17} are weakly decreasing and the rules in {1-3,6,19} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.42 seconds) --- May 4, 2006